home *** CD-ROM | disk | FTP | other *** search
/ Turnbull China Bikeride / Turnbull China Bikeride - Disc 1.iso / ARGONET / PD / PROGRAMMING / LCLINT2.SPK / test / test_a / db2 / h / empset < prev    next >
Text File  |  1996-11-15  |  940b  |  41 lines
  1. # ifndef EMPSET_H
  2. # define EMPSET_H
  3.  
  4. # include "eref.h"
  5. # include "erc.h"
  6. # include "ereftab.h"
  7.  
  8. typedef erc empset;
  9.  
  10. ereftab known;
  11.  
  12. /*
  13.   Abstraction function, toEmpSet:
  14.     e \in toEmpSet(s) ==
  15.       exists er (count(er, s.val) = 1
  16.         /\ getERef(known, e) = er)
  17.  
  18.   Rep invariant:
  19.     forall s: empset
  20.       (forall er: eref (count(er, s.val) <= 1)
  21.       /\ s.activeIters = 0
  22.       /\ forall er: eref (count(er, s.val) = 1
  23.         => in(known, er)))
  24. */
  25.  
  26. # include "lh.empset"
  27.  
  28. # define empset_create()  (erc_create())
  29. # define empset_final(s) (erc_final(s))
  30. # define empset_member(e, s) \
  31.          (!(eref_equal(_empset_get(e, s), erefNIL)))
  32. # define empset_size(es) (erc_size(es))
  33. # define empset_choose(es) (eref_get(erc_choose(es)))
  34. # define empset_sprint(es) (erc_sprint(es))
  35.  
  36. #define empset_elements(e, m_x) \
  37.    erc_elements(e, m_y) { employee m_x = eref_get(m_y);
  38. #define end_empset_elements        } end_erc_elements
  39.  
  40. # endif
  41.